Nuprl Lemma : R-rframe-rule
11,40
postcript
pdf
i
,
x
:Id,
L
:(Knd List). Rrframe(
i
;
x
;
L
) ||-
es
.@
i
: only members of
L
read
x
latex
Definitions
t
T
,
True
,
P
Q
,
R-Feasible(
R
)
,
P
&
Q
,
R
||-
es
.
P
(
es
)
,
x
:
A
.
B
(
x
)
,
Consistent(
R
;
es
)
,
Lemmas
Id
wf
,
Knd
wf
,
event
system
wf
,
Rrframe
wf
,
R-consistent
wf
origin
i, x:Id, L:(Knd List). Rrframe(i;x;L) ||- es.@i: only members of L read x i, x:Id, L:(Knd List). Rrframe(i;x;L) ||- es.@i: only members of L read x 
T
Qx:A. B(x)